$\forall$$A$, $B$:Type, $R$:($A$$\rightarrow$$A$$\rightarrow\mathbb{P}$), $S$:($B$$\rightarrow$$B$$\rightarrow\mathbb{P}$), $f$:($A$$\rightarrow$$B$).
\\[0ex]Inj($A$;$B$;$f$)
\\[0ex]$\Rightarrow$ RelsIso($A$;$B$;$x$,$y$.$R$($x$,$y$);$x$,$y$.$S$($x$,$y$);$f$)
\\[0ex]$\Rightarrow$ AntiSym($B$;$x$,$y$.$S$($x$,$y$))
\\[0ex]$\Rightarrow$ AntiSym($A$;$x$,$y$.$R$($x$,$y$))